es:ES, i:Id, L:(IdLnk List), T:(IdType).
es-secret-server{table:ut2, encrypt:ut2, decrypt:ut2}
es-secret-server(es; T; L; i)
 (e2, e1:E.
 (loc(e1) = i)  (e1 <loc e2)  (ptr(("table" after e1))  ptr("table" when e2))) 

latex

Definitions

False, let x,y,z = a in t(x;y;z), t.2, t.1, A  B, ptr(tab), encrypt(tab;keyv), A, (state when e), s.x, Top, P  Q, P  Q, Knd, True, T, x. t(x), , t  T, P & Q, "$x", (e <loc e'), P  Q, Id, x:A. B(x), secret-table(T), @i events of kind k change x to f State(ds) (val:T), e@i. P(e), xL. P(x), x:A. B(x), Dec(P), SQType(T), P  Q, @i(x:T), {T}, x(s), WellFnd{i}(A;x,y.R(x;y)), @i only L affect x:T, A c B, , let x = a in b(x), es-secret-server

Lemmas

id-deq wf, fpf-cap-single1, es-loc-rcv, ldst wf, lsrc wf, es-kind-rcv, es-isrcv-loc, member map, rcv wf, Knd wf, map wf, decidable equal Kind, es-kind wf, decidable l member, Id sq, true wf, squash wf, es-after-pred, event system wf, IdLnk wf, Id wf, es-secret-server wf, es-E wf, es-locl wf, es-pred-locl, es-pred wf, es-locl-iff, es-loc-pred, es-when wf, nat wf, st-ptr wf, secret-table wf, es-vartype wf, es-after wf, le wf, es-causl wf, es-loc wf, es-locl-wellfnd